Section: Contracts and Grants with Industry

ANR project DeCert

Participants : Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo.

The DeCert (Deduction and Certification) project is being funded by ANR from 2009–2012 within its “Domaines émergents” program. It is coordinated by the Celtique project team of INRIA Rennes, the other partners are academic teams from INRIA Saclay (Proval) and INRIA Sophia Antipolis (Marelle) as well as the CEA and the Systerel company. In Nancy, the project also involves members of the Cassis team, in particular Alain Giorgetti and Christophe Ringeissen.

The objective of the project is to study certified decision procedures, including the design of appropriate certificates, the development of new certifying decision procedures, their combination, their integration with skeptical proof assistants such as Coq or Isabelle, and their use in application domains such as software verification or static analysis. The main lines of research concern questions of expressiveness vs. efficiency, certificates vs. proof objects, and the integration of certificates into verification environments. Our work within the project is related to veriT (see section  5.1 ), its proof production, and its integration with verification environments such as Isabelle or the TLA⁺ proof environments (see section  5.2 ).